The present invention relates to the verification of the timing behavior in embedded systems. More particularly, the invention provides techniques for determining whether it is impossible for an event to be dropped in such a system.
Embedded systems, i.e., systems embedded in the equipment they serve, typically consist of several interacting components that constantly monitor and react to various conditions (sometimes referred to as "external events") in their respective environments. Due to flexibility and cost-efficiency, many of these components are often implemented in software and executed on a controller (i.e., processor) for the system. Each component is implemented as a software task (sometimes referred to as an "internal task"), and an operating system is used to schedule execution of tasks. Embedded systems are being increasingly used for a variety of products, including low-cost high-volume consumer products.
FIG. 1A illustrates a typical environment for an embedded system. An apparatus 10 includes an embedded system 11, a sensor 12, and an actuator 13. Embedded system 11 includes a processor 14 and a storage medium 15. Storage medium 15 stores one or more tasks 16 which execute on processor 14.
Sensor 12 sends signals to system 11 indicating the occurrence of one of a set of one or more external events. Typically, sensor 12 monitors one or more characteristics of the environment of apparatus 10 (such as temperature or pressure) and each of one or more of the external events occurs whenever sensor 12 detects that the environment of apparatus 10 is in a particular state. Other external events may occur whenever sensor 12 detects a condition unrelated to the environment of apparatus 10 (such as expiration of a timeout period).
Each of tasks 16 becomes ready for execution upon the occurrence of any of one or more of the external events and/or upon the completion of execution of any of one or more of tasks 16. One or more of tasks 16 cause processor 14 to send digital data to actuator 13 which takes some physical action in response to the data received (such as moving a component in apparatus 10, changing a characteristic of the environment of apparatus 10 such as temperature or pressure, providing a voltage or current, etc).
To verify the correctness of software tasks in an embedded system, one must verify their functionality and their timing behavior. The timing behavior depends on timing properties of tasks and external events, as well as the scheduling policy: i.e., the set of rules determining which task to execute on the processor, if more than one task is ready to run. Consequently, the timing verification problem for such systems is sometimes referred to as the schedule validation problem. Given that embedded systems are becoming more complex and controlling ever more critical processes, schedule validation is becoming a dominant consideration in embedded system design beside cost, performance, and power consumption.
Each internal task is enabled (i.e., ready to commence execution) upon the occurrence of one or more external events, and/or upon the completion of one or more of the other internal tasks. Each external event is hereinafter described as the completion of an external task (whose duration, unlike that of an internal task, is of no relevance to the timing verification issues discussed herein). An embedded system is said to include an event (i,j) if completion of task i enables internal task j. Event (i,j) is referred to as internal or external depending on whether task i is internal or external. One aspect of schedule validation involves determining whether or not an event can be dropped. Event (i,j) can be dropped if in some execution of the embedded system it is possible, after task i completes execution, for task i to complete execution again before task j completes execution.
Dropping certain events (designated as "critical") may not be acceptable. For example, an embedded system used to calculate the speed of a wheel from a counter keeping track of the number of wheel revolutions, might include an external task i that completes execution once every revolution of the wheel by sending a signal to the system controller, and an internal task j that is enabled upon every completion of the external task and whose purpose is to increment the counter by one. If event (i,j) is dropped, in other words if two completions of external task i (i.e., two revolutions of the wheel) occur without an intervening completion of internal task j, the first wheel revolution will not result in an increment to the counter, and thus an incorrect wheel speed will be computed.
The timing behavior of an embedded system is verified to be correct (i.e., the schedule of the embedded system is proved valid) if it is determined that none of the critical events in the embedded system can be dropped. Two of the most widely used methods for schedule validation are simulation and prototyping. In prototyping, a physical model of an embedded system is built, typically comprising a microprocessor or micro-controller, memory, and some interface circuitry. The prototype is then exercised with some set of input sequences of external events, and the outputs of the system are monitored for correctness. Simulation is similar, except that hardware components (microprocessor, memory, etc,) are replaced with corresponding simulation models.
Because there are an infinite number of possible input sequences of external events to an embedded system, prototyping and simulation are techniques that cannot prove schedule validity. Thus, even if the system behaves correctly for all sequences in the test set, there are no guarantees that the system will behave correctly for all other input sequences. In other words, using these methods, a schedule can be proved invalid, but it can never be proved valid.
Several techniques of general applicability have been proposed for analytically determining whether a schedule of an embedded system is valid. However, these techniques require an execution time that grows exponentially with the size of the embedded system (i.e., number of tasks), and are thus impractical for all but the smallest embedded systems.
Yet other computationally tractable but less general schedule validation techniques have been proposed. In particular, each of these techniques can, at most, only be applied to embedded systems satisfying the following constraints:
(a) completion of each task enables at most one other internal task. This constraint severely limits the ability to share information between the system tasks, because completion of any task can trigger the execution of at most one other task. PA1 (b) each internal task is enabled by the completion of exactly one other task. This constraint severely limits the ability to realistically model reactive real-time systems, because such systems usually include one or more components that are executed in response to any one of two or more events in their environment. PA1 (c) an internal task is not allowed to execute whenever any of its successor tasks are enabled (a task is a successor to a given task if the task is enabled by the completion of the given task). This constraint makes it impossible for internal events to be dropped, and may, for example, be unsuitable for systems having urgent tasks that must be executed promptly even if one or more of their successor tasks are enabled.
What would be desirable is an efficient analytical technique of general applicability for proving that an event cannot be dropped in any execution of an embedded system.